es:ES, a, b:E. first(a)  first(b)  pred(a) = pred(b)  E  a = b 

latex

Definitions	False, P  Q, A, t  T, x:A. B(x), P & Q, P  Q, e  e' , P  Q, True, T, ES, loc(e), Id, first(e), b, pred(e), Prop, (e <loc e'), E, P  Q
Lemmas	es-pred wf, not wf, assert wf, es-first wf, es-axioms, es-loc-pred, Id wf, es-loc wf, squash wf, true wf, es-E wf, event system wf, es-le wf, es-le-pred, es-locl-antireflexive